es-decls(es;i;ds;da)
== l-all(fpf-domain(ds); x.let T = fpf-ap(ds; id-deq; x) in subtype_rel(es-vartype(es; i; x); T))
==  l-all(fpf-domain(da);
==  l-all(k.let T = fpf-ap(da; Kind-deq; k) in
==  l-all(k.let Te:es-E(es). 
==  l-all(k.let ((loc(e) = i)  (es-isrcv(es; e)))
==  l-all(k.let  (es-kind(es; e) = k)
==  l-all(k.let  subtype_rel(es-valtype(es; e); T)) 

latex

---

clarification:

es-decls(es;i;ds;da)
== l-all(fpf-domain(ds); x.let T = fpf-ap(ds; id-deq; x) in subtype_rel(es-vartype(es; i; x); T))
==  l-all(fpf-domain(da);
==  l-all(k.let T = fpf-ap(da; Kind-deq; k) in
==  l-all(k.let Te:es-E(es). 
==  l-all(k.let ((es-loc(es; e) = i  Id)  (es-isrcv(es; e)))
==  l-all(k.let  (es-kind(es; e) = k  Knd)
==  l-all(k.let  subtype_rel(es-valtype(es; e); T)) 

latex

Definitions	P  Q, id-deq, es-vartype(es; i; x), l-all(L; x.P(x)), fpf-domain(f), let x = a in b(x), fpf-ap(f; eq; x), Kind-deq, x:A. B(x), es-E(es), P  Q, Id, loc(e), b, es-isrcv(es; e), P  Q, s = t, Knd, es-kind(es; e), es-valtype(es; e)
FDL editor aliases	es-decls